COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	KNOWAX started.
C00008 00003	WISEMEN started.
C00011 ENDMK
C⊗;
KNOWAX started.
* 
* 
* 
* 
* 
* 
* 
* 
* 
* 
* 
* 12. ∀P Q.TRUE1 P AND1 Q≡TRUE1 P∧TRUE1 Q
    ctxt: (3 6 9)   deps: NIL

* 13. ∀P Q.TRUE1 P OR1 Q≡TRUE1 P∨TRUE1 Q
    ctxt: (4 6 9)   deps: NIL

* 14. ∀P Q.TRUE1 P IMPLIES1 Q≡TRUE1 P⊃TRUE1 Q
    ctxt: (2 6 9)   deps: NIL

* 15. ∀P.TRUE1 NOT1 P≡¬TRUE1 P
    ctxt: (5 6 9)   deps: NIL

* 16. ∀P Q.TRUE1 P EQUIV1 Q≡(TRUE1 P≡TRUE1 Q)
    ctxt: (1 6 9)   deps: NIL

* 17. ∀S P.TRUE1 S*P IMPLIES1 P
    ctxt: (2 6 7 9 10)   deps: NIL

* 18. ∀S P.TRUE1 0*(S*P IMPLIES1 P)
    ctxt: (2 6 7 9 10 11)   deps: NIL

* 19. ∀S P.TRUE1 0*(0*P IMPLIES1 0*(S*P))
    ctxt: (2 6 7 9 10 11)   deps: NIL

* 20. ∀S P Q.TRUE1 0*(S*P AND1 S*(P IMPLIES1 Q) IMPLIES1 S*Q)
    ctxt: (2 3 6 7 9 10 11)   deps: NIL

* 21. ∀P Q.TRUE1 0*(P IMPLIES1 (Q IMPLIES1 P))
    ctxt: (2 6 7 9 11)   deps: NIL

* 22. ∀P Q R.TRUE1 0*
                 ((R IMPLIES1 (P IMPLIES1 Q)) AND1 (R IMPLIES1 P) IMPLIES1 
                  (R IMPLIES1 Q))
    ctxt: (2 3 6 7 9 11)   deps: NIL

* 23. ∀P.TRUE1 0*(NOT1 (NOT1 P) IMPLIES1 P)
    ctxt: (2 5 6 7 9 11)   deps: NIL

* 24. ∀S P.TRUE1 0*(S*P IMPLIES1 S*(S*P))
    ctxt: (2 6 7 9 10 11)   deps: NIL

* 25. ∀S P.TRUE1 0*(NOT1 S*P IMPLIES1 S*(NOT1 S*P))
    ctxt: (2 5 6 7 9 10 11)   deps: NIL

* 26. ∀S P.TRUE1 0*(S$P EQUIV1 S*P OR1 S*(NOT1 P))
    ctxt: (1 4 5 6 7 8 9 10 11)   deps: NIL

* 
;;; know.lsp[f81,jmc]	ekl axioms for knowledge

(proof knowax)

(decl (equiv1) |proposition⊗proposition → proposition| constant nil infix 830)

(decl (implies1) |proposition⊗proposition → proposition| constant nil infix 840)

(decl (and1) |proposition⊗proposition* → proposition| functional nil infix 860 both)

(decl (or1) |proposition⊗proposition* → proposition| functional nil infix 850 both)

(decl (not1) |proposition → proposition| constant nil unary 870)

(decl (true1) |proposition → truthval| constant nil unary 820)

(decl (*) |person⊗proposition → proposition| constant nil infix 875)

(decl ($) |person⊗proposition → proposition| constant nil infix 875)

(decl (p p0 p1 p2 q q0 q1 q2 r r0 r1 r2) proposition variable proposition)

(decl (S S0 S1 S2) person variable person)

(decl (0) person constant person)


;;; definitions of imitation propositional operators

(axiom |∀p q.true1(p and1 q) ≡ true1(p) ∧ true1(q)|)

(axiom |∀p q.true1(p or1 q) ≡ true1(p) ∨ true1(q)|)

(axiom |∀p q.true1(p implies1 q) ≡ true1(p) ⊃ true1(q)|)

(axiom |∀p.true1(not1 p) ≡ ¬true1 p|)

(axiom |∀p q.true1(p equiv1 q) ≡ (true1(p) ≡ true1(q))|)


;;; modal knowledge axioms

(axiom |∀S p.true1 S * p implies1 p|)

(axiom |∀S p.true1 0*(S*p implies1 p)|)

(axiom |∀S p.true1 0*(0*p implies1 0*(S*p))|)

(axiom |∀S p q.true1 0*(S*p and1 S*(p implies1 q) implies1 S*q)|)


;;; even fools know tautologies

(axiom |∀p q.true1 0*(p implies1 (q implies1 p))|)

(axiom |∀p q r.true1 0*((r implies1 (p implies1 q)) and1
(r implies1 p) implies1 (r implies1 q))|)

(axiom |∀p.true1 0*(not1 not1 p implies1 p)|)


;;; introspective axioms (not always used)

(axiom |∀S p.true1(0*(S*p implies1 S*(S*p)))|)

(axiom |∀S p.true1(0*(not1 S*p implies1 S*(not1 S*p)))|)

;;; knowing whether

(axiom |∀S p.true1 0*(S$p equiv1 S*p or1 S*(not1 p))|)
WISEMEN started.
* 
* 
* 
* 3. TRUE1 WHITE1 AND1 WHITE2 AND1 WHITE3
   ctxt: (2 KNOWAX#3 KNOWAX#6)   deps: NIL

* 4. TRUE1 0*(WHITE1 OR1 WHITE2 OR1 WHITE3)
   ctxt: (2 KNOWAX#4 KNOWAX#6 KNOWAX#7 KNOWAX#11)   deps: NIL

* 5. TRUE1 0*
         (WISE1$WHITE2 AND1 WISE1$WHITE3 AND1 WISE2$WHITE1 AND1 
          WISE2$WHITE3 AND1 WISE3$WHITE1 AND1 WISE3$WHITE2)
   ctxt: (1 2 KNOWAX#3 KNOWAX#6 KNOWAX#7 KNOWAX#8 KNOWAX#11)   deps: NIL

* 6. TRUE1 WISE3*(WISE2*(NOT1 WISE1*WHITE1))
   ctxt: (1 2 KNOWAX#5 KNOWAX#6 KNOWAX#7)   deps: NIL

* 7. TRUE1 WISE3*(NOT1 WISE2*WHITE2)
   ctxt: (1 2 KNOWAX#5 KNOWAX#6 KNOWAX#7)   deps: NIL

* 
;;; problem of three wise men

(proof wisemen)

(context knowax#1:*)

(decl (wise1 wise2 wise3) person constant person)

(decl (white1 white2 white3) proposition constant proposition)

(axiom |true1(white1 and1 white2 and1 white3)|)

(axiom |true1 0*(white1 or1 white2 or1 white3)|)

(axiom |true1 0*(wise1$white2 and1 wise1$white3 and1 wise2$white1
and1 wise2$white3 and1 wise3$white1 and1 wise3$white2)|)

(axiom |true1 wise3*(wise2*(not1 wise1*white1))|)

(axiom |true1 wise3*(not1 wise2*white2)|)

;;; The goal is now to prove |true1 wise3*white3|

;;; It should be a tautology once the right instantiations of the
;;; axioms have been made.

;;; The modal proof won't necessarily be easy.
;;; The first step may be to show tautology(p) ⊃ 0*p.